Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		minus(n__0,Y)	→ 0
2:		minus(n__s(X),n__s(Y))	→ minus(activate(X),activate(Y))
3:		geq(X,n__0)	→ true
4:		geq(n__0,n__s(Y))	→ false
5:		geq(n__s(X),n__s(Y))	→ geq(activate(X),activate(Y))
6:		div(0,n__s(Y))	→ 0
7:		div(s(X),n__s(Y))	→ if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0)
8:		if(true,X,Y)	→ activate(X)
9:		if(false,X,Y)	→ activate(Y)
10:		0	→ n__0
11:		s(X)	→ n__s(X)
12:		activate(n__0)	→ 0
13:		activate(n__s(X))	→ s(X)
14:		activate(X)	→ X

There are 16 dependency pairs:


15:		MINUS(n__0,Y)	→ 0#
16:		MINUS(n__s(X),n__s(Y))	→ MINUS(activate(X),activate(Y))
17:		MINUS(n__s(X),n__s(Y))	→ ACTIVATE(X)
18:		MINUS(n__s(X),n__s(Y))	→ ACTIVATE(Y)
19:		GEQ(n__s(X),n__s(Y))	→ GEQ(activate(X),activate(Y))
20:		GEQ(n__s(X),n__s(Y))	→ ACTIVATE(X)
21:		GEQ(n__s(X),n__s(Y))	→ ACTIVATE(Y)
22:		DIV(s(X),n__s(Y))	→ IF(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0)
23:		DIV(s(X),n__s(Y))	→ GEQ(X,activate(Y))
24:		DIV(s(X),n__s(Y))	→ DIV(minus(X,activate(Y)),n__s(activate(Y)))
25:		DIV(s(X),n__s(Y))	→ MINUS(X,activate(Y))
26:		DIV(s(X),n__s(Y))	→ ACTIVATE(Y)
27:		IF(true,X,Y)	→ ACTIVATE(X)
28:		IF(false,X,Y)	→ ACTIVATE(Y)
29:		ACTIVATE(n__0)	→ 0#
30:		ACTIVATE(n__s(X))	→ S(X)

The approximated dependency graph contains 3 SCCs: {19}, {16} and {24}.

Consider the SCC {19}. The usable rules are {10-14}. The constraints could not be solved.

Consider the SCC {16}. The usable rules are {10-14}. The constraints could not be solved.

Consider the SCC {24}. The usable rules are {1,2,10-14}. By taking the AF π with π(DIV) = 1 and π(minus) = π(n__s) = π(s) = [ ] together with the lexicographic path order with precedence activate ≻ s ≻ minus ≻ 0 ≻ n__0 and s ≻ n__s, rule 2 is weakly decreasing and the rules in {1,10-14,24} are strictly decreasing.

Tyrolean Termination Tool (0.08 seconds) --- May 3, 2006